Towards Инфинити Категории
Из серии давно забытых срачей. Когда-то Жорж, автор учебника по Теории Категорий решительно громко хлопнул дверью и ушел из "всем похуй" камюнити в ЖЖ про теоркат, с которого начался теоркат в ЖЖ (ну пиздежь конечно) https://category-theory.livejournal.com/34284.html Спустя годы в условиях жесткой изоляции коммуникаций по предмету решил зайти на https://dxdy.ru/topic127434.html и задать вопрос про 2-категории и бикатегории, вопрос их изоморфизма произведению категорий. И что вы думаете — мне ответил Жорж! Посмотрим как будет разворачиваться борьба. Включайте подписку HBO!
Cat: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
Ob: U = precategory
Hom (A B: Ob): U = catfunctor A B
id (A: Ob): catfunctor A A = idFunctor A
c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = compFunctor A B C f g
...
Func (X Y: precategory): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
Ob: U = catfunctor X Y
Hom (A B: Ob): U = ntrans X Y A B
id (A: Ob): ntrans X Y A A = ...
c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = ...
...
Cat2 : U
= (Ob: U)
* (Hom: (A B: Ob) -> U)
* (Hom2: (A B: Ob) -> (C F: Hom A B) -> U)
* (id: (A: Ob) -> Hom A A)
* (id2: (A: Ob) -> (B: Hom A A) -> Hom2 A A B B)
* (c: (A B C: Ob) (f: Hom A B) (g: Hom B C) -> Hom A C)
* (c2: (A B: Ob) (X Y Z: Hom A B)
(f: Hom2 A B X Y) (g: Hom2 A B Y Z) -> Hom2 A B X Z)
* ...
Cat2Impl1 : Cat2
= ( {- Ob -} Cat.1.1,
{- Hom -} \ (X Y: Cat.1.1) -> (Func X Y).1.1,
{- Hom2 -} \ (X Y: Cat.1.1) -> (Func X Y).1.2,
{- id -} Cat.2.1,
{- id2 -} \ (A: Cat.1.1) -> (Func A A).2.1,
{- c -} Cat.2.2.1,
{- c2 -} \ (X Y: Cat.1.1) -> (Func X Y).2.2.1,
... )
[1]. mltt/types/category/
[2]. category.ctt